functor Vc (S : VC_STRUCTS) : VC =
struct
  open S

  type id = string
  type arraysize = int

  structure S = Set.StringBSet

  structure Coqlib = Coqlib ()

  structure E = ErrorMsg
  val error = E.error

  datatype binop
    = Plus
    | Minus
    | Times
    | Divide
    | Modus
    | Band
    | Bor
    | Equ
    | NEqu
    | GT
    | GE
    | LT
    | LE

  datatype mytype
    = Int
    | Bool
    | Void
    | Struct of string
    | Pointer of mytype
    | Array of arraysize * mytype

  fun tpCompare (tp1, tp2) =
      case (tp1, tp2)
       of (Int, Int) => EQUAL
        | (Bool, Bool) => EQUAL
        | (Void, Void) => EQUAL
        | (Struct s1, Struct s2) => String.compare (s1, s2)
        | (Pointer ty1, Pointer ty2) => tpCompare (ty1, ty2)
        | (Array (i1, ty1), Array (i2, ty2)) =>
          (case Int.compare (i1, i2)
            of EQUAL => tpCompare (ty1, ty2)
             | a => a)(*?*)
        | (_, _) => LESS(*?*)

  datatype exp
    = Expvoid
    | IntNum of int
    | True
    | False
    | Null
    | Lval of lval
    | BinopExp of exp * binop * exp
    | Not of exp
    | Imply of exp * exp
    | Forall of id * mytype * exp
    | Exists of id * mytype * exp
    | Pi of lval list list
    | N of lval list
    | D of lval list
    | Prev of lval
    | LList of exp
    | Tree of exp
    | Pred of id * exp(*?*)
    | Let of exp * exp * exp

  and lval
    = Var of id
    | Ptr of lval * lval(*?*)
    | Sharp of mytype
    | Inarray of lval * exp
    | Instruct of lval * id
    | Instruct2 of lval * id * id(*?*)
    | Upd of lval * exp * exp
    | Sel of lval * exp

  fun compare (lval1, lval2) =
      case (lval1, lval2)
       of (Var id1, Var id2) => String.compare (id1, id2)
        | (Instruct (lval11, id), Instruct2 (lval22, id1, id2)) =>
          (case (compare (lval11, lval22), String.compare (id, id2))
            of (EQUAL, EQUAL) => EQUAL
             | _ => LESS)
        | (Instruct2 (lval11, id1, id2), Instruct (lval22, id)) =>
          (case (compare (lval11, lval22), String.compare (id, id2))
            of (EQUAL, EQUAL) => EQUAL
             | _ => LESS)
        | (Var id, Instruct2 (Ptr (_, Var idi), id1, id2)) =>
          String.compare (id, idi)
        | (Instruct2 (Ptr (_, Var idi), id1, id2), Var id) =>
          String.compare (idi, id)
        | (x1, x2) =>
          if x1 = x2
      	  then EQUAL
          else LESS

  fun twoLongIds1 () = (Var "x", Instruct2 (Ptr (Sharp (Int), Var "x"), "next", "i"))
  fun twoLongIds () = (Var "x", Instruct2 (Ptr (Sharp (Int), Var "y"), "next", "i"))

  fun isPrefix (lval1, lval2) =
      case (lval1, lval2)
       of (Var id1, Instruct (Ptr (x, Var id2), id3)) =>
          (case String.compare (id1, id2)
            of EQUAL => true
             | _ => false)
        | (_, _) => false

  fun subst (lval1, lval2, sub) =
      case (lval1, lval2, sub)
       of (Var id1, Instruct (Ptr (x, Var id2), id3), Var id4) =>
          (case String.compare (id1, id2)
            of EQUAL => Instruct (Ptr (x, Var id4), id3)
             | _ => lval2)
        | (_, _, _) => lval2

  fun substDel (lval1, lval2) =
      case (lval1, lval2)
       of (Var id1, Instruct (Ptr (x, Var id2), id3)) =>
          (case String.compare (id1, id2)
            of EQUAL => Var "@@@Del"
             | _ => lval2)
        | (_, _) => lval2

  val isStruct2 = fn Instruct2 _ => true
                   | _ => false

  fun struct22id lval =
      case lval
       of Instruct2 (Ptr (_, lval1), id1, id2) => lval1
        | _ => lval

  fun op2str b =
      case b
       of Plus => " + "
        | _ => (print "not impl yet\n"; "")
  fun exp2str exp =
      case exp
       of Expvoid => "()"
        | IntNum i => Int.toString i
        | True => "true"
        | False => "false"
        | Null => "null"
        | Lval lval => lval2str lval
        | BinopExp (e1, b, e2) => (exp2str e1)^(op2str b)^(exp2str e2)
        | Not e => "!"^(exp2str e)
        | _ => (print "not impl in vc.fun: 128:\n"; "")
  and lval2str lval = "\""^(lval2str1 lval)^"\""
  and lval2str1 lval =
      case lval
        of Var id => id
         | Ptr (lval1, lval2) => "*"^(lval2str1 lval2)
         | Sharp ty => ""
         | Inarray(lval, e) => (lval2str1 lval)^"[...]"
         | Instruct (Ptr(lval1, lval2), id) => (lval2str1 lval2)^"->"^id
         | Instruct (lval, id) => (lval2str1 lval)^"."^id
         | Instruct2 (Ptr(lval1, lval2), id1, id2) => String.concat [lval2str1 lval2, "(->", id1, ")", id2]
         | Instruct2 (lval, id1, id2) => String.concat [lval2str1 lval, "(->", id1, ")", id2]
         | _ => (print "not in vc.fun: L140\n"; "")

  fun ckE' e =
      case e
        of Expvoid => ()
         | IntNum(i) => ()
         | True => ()
         | False => ()
         | Null => ()
         | Lval lval => ckL lval
         | BinopExp(e1, b, e2) => (ckE' e1; ckE' e2)
         | Not(e) => ckE' e
         | Imply(e1, e2) => (ckE' e1; ckE' e2)
         | Forall(id, ty, e) => (ckE' e)
         | Exists(id, ty, e) => (ckE' e)
         | _ => raise Fail ("not implemented yet\n")

  and ckE e =
      case e
        of Expvoid => ()
         | IntNum(i) => ()
         | True => ()
         | False => error 0 " errors in verification phase, this program is not valid\n"
         | Null => ()
         | Lval(lval) => ckL lval
         | BinopExp(e1, b, e2) => (ckE' e1; ckE' e2)
         | Not e => ()
         | Imply(e1, e2) =>
              if e2 = False
              then ()(*error 0 "verification fail: this program is NOT valid\n"*)
              else ()
         | Forall(id, ty, e) => ()
         | Exists(id, ty, e) => ()
         | _ => raise Fail ("not implemented yet\n")

  and ckL lval =
      case lval
       of Var id  => ()
        | Upd (lval, e1, e2) => ()
        | Sel (lval, Null) => error 0 " errors in verification phase: null pointer dereference\n"
        | Sel (lval, e) => (ckL lval; ckE' e)
        | Sharp ty => ()
        | Ptr (lval1, lval2) => ()
        | _ => raise Fail ("should not happen this var...\n")

  val opt2 = ref true
  fun close_opt2 () = (opt2 := false)
  fun open_opt2 () = (opt2 := true)

  fun lift b =
      if b
      then True
      else False

  fun opt_e e =
      let fun tr (Expvoid) = Expvoid
            | tr (IntNum(i)) = IntNum(i)
            | tr (True) = True
            | tr (False) = False
            | tr (Null) = Null
            | tr (BinopExp(IntNum(0), Plus, e2)) = opt_e e2
            | tr (BinopExp(IntNum(i), Plus, IntNum(j))) = IntNum(i+j)
            | tr (BinopExp(IntNum(i), Minus, IntNum(j))) = IntNum(i-j)
            | tr (BinopExp(IntNum(0), Times, e2)) = IntNum(0)
            | tr (BinopExp(IntNum(i), Times, IntNum(j))) = IntNum(i*j)
            | tr (BinopExp(IntNum(0), Divide, e2)) = IntNum(0)
            | tr (BinopExp(IntNum(i), Divide, IntNum(j))) = IntNum(i div j)
            | tr (BinopExp(IntNum(0), Modus, e2)) = IntNum(0)
            | tr (BinopExp(IntNum(i), Modus, IntNum(j))) = IntNum(i mod j)
            | tr (BinopExp(True, Band, e2)) = opt_e e2
            | tr (BinopExp(False, Band, e2)) = False
            | tr (BinopExp(e1, Band, True)) = opt_e e1
            | tr (BinopExp(e1, Band, False)) = False
            | tr (BinopExp(x as BinopExp(e11, GE, e12), Band, y as BinopExp(e21, GE, e22))) =
              if x=y
              then opt_e x
              else if e11=e22 andalso e12=e21
                   then BinopExp(e11, Equ, e12)
                   else BinopExp(opt_e x, Band, opt_e y)
            | tr (e as BinopExp(e1, Band, e2)) =
              if e1 = e2
              then opt_e e1
              else BinopExp(opt_e e1, Band, opt_e e2)
            | tr (BinopExp(True, Bor, e2)) = True
            | tr (BinopExp(False, Bor, e2)) = opt_e e2
            | tr (BinopExp(e1, Bor, e2)) = BinopExp(opt_e e1, Bor, opt_e e2)
              (*--------------------------eq--------------------------*)
            | tr (BinopExp(IntNum(i), Equ, IntNum(j))) = lift(i=j)
            | tr (BinopExp(e1, Equ, e2)) =
              if (e1 = e2)
              then lift (true)
              else let val (e1', e2') = (opt_e e1, opt_e e2)
                   in  BinopExp(e1', Equ, e2')
                   end
              (*-------------------------neq--------------------------*)
            | tr (BinopExp(IntNum(i), NEqu, IntNum(j))) = lift(i<>j)
            | tr (BinopExp(e1, NEqu, e2)) =
              if (e1 = e2)
              then lift (false)
              else let val (e1', e2') = (opt_e e1, opt_e e2)
                   in  BinopExp(e1', NEqu, e2')
                   end
              (*------------------------- gt -------------------------*)
            | tr (BinopExp(IntNum(i), GT, IntNum(j))) = lift(i>j)
            | tr (BinopExp(e1, GT, e2)) =
              if (e1 = e2)
              then lift (false)
              else let val (e1', e2') = (opt_e e1, opt_e e2)
                   in  BinopExp(e1', GE, BinopExp(e2', Plus, IntNum(1)))
                   end
              (*------------------------- ge -------------------------*)
            | tr (BinopExp(IntNum(i), GE, IntNum(j))) = lift(i>=j)
            | tr (BinopExp(e1, GE, e2)) =
              if (e1 = e2)
              then lift (true)
              else let val (e1', e2') = (opt_e e1, opt_e e2)
                   in  BinopExp(e1', GE, e2')
                   end
              (*------------------------- lt -------------------------*)
            | tr (BinopExp(IntNum(i), LT, IntNum(j))) = lift(i<j)
            | tr (BinopExp(e1, LT, e2)) =
              if (e1 = e2)
              then lift (false)
              else let val (e1', e2') = (opt_e e1, opt_e e2)
                   in  opt_e (BinopExp(e2', GT, e1'))
                   end
              (*------------------------- le -------------------------*)
            | tr (BinopExp(IntNum(i), LE, IntNum(j))) = lift(i<=j)
            | tr (BinopExp(e1, LE, e2)) =
              if (e1 = e2)
              then lift (true)
              else let val (e1', e2') = (opt_e e1, opt_e e2)
                   in  opt_e (BinopExp(e2', GE, e1'))
                   end
              (*------------------------- binop -------------------------*)
            | tr (BinopExp(e1, b, e2)) =
              let val (e1', e2') = (opt_e e1, opt_e e2)
              in  BinopExp(e1', b, e2')
              end
              (*--------------------------not--------------------------*)
            | tr (Not(True)) = False
            | tr (Not(False)) = True
            | tr (Not(BinopExp(e1, Equ, e2))) = BinopExp(opt_e e1, NEqu, opt_e e2)
            | tr (Not(BinopExp(e1, NEqu, e2))) = BinopExp(opt_e e1, Equ, opt_e e2)
            | tr (Not(BinopExp(e1, GT, e2))) = BinopExp(opt_e e1, LE, opt_e e2)
            | tr (Not(BinopExp(e1, GE, e2))) = BinopExp(opt_e e1, LT, opt_e e2)
            | tr (Not(BinopExp(e1, LT, e2))) = BinopExp(opt_e e1, GE, opt_e e2)
            | tr (Not(BinopExp(e1, LE, e2))) = BinopExp(opt_e e1, GT, opt_e e2)
            | tr (Not(e)) = Not(opt_e e)
              (*------------------------- lval -------------------------*)
            (*| tr (Lval(Sel(Upd(lval, e1, e2), e3))) =
              if e1=e3
              then e2
              else Lval(Sel(lval, e3))*)
            | tr (Lval(lval)) = opt_l lval
              (*------------------------- imply -------------------------*)
            | tr (Imply(False, e2)) = True
            | tr (Imply(e1, True)) = True
            | tr (Imply(True, e2)) = opt_e e2
            | tr (Imply(e1, Imply(e2, e3))) = Imply(BinopExp(e1, Band, e2), e3)
            | tr (Imply(x as (BinopExp(e1, Band, e2)), y as (BinopExp(e3, Band, e4)))) =
              if x=y
              then True
              else if e1=e4 andalso e2=e3
                   then True
                   else Imply(opt_e x, opt_e y)
            | tr (Imply(e1, e2)) =
              if e1=e2
              then True
              else Imply(opt_e e1, opt_e e2)
              (*-------------------------- forall -------------------------*)
            | tr (Forall(tid, ty, True)) = True
            | tr (Forall(tid, ty, False)) = False
            | tr (Forall(tid, ty, e1)) = Forall(tid, ty, opt_e e1)
              (*-------------------------- exists -------------------------*)
            | tr (Exists(tid, ty, e1)) = Exists(tid, ty, opt_e e1)
            | tr (Prev(lval)) = raise Fail "not implemented yet...prev" (* all other cases are ignored for now... -Baojian*)
            | tr (Pi(lvalss)) = raise Fail "pi"
            | tr (N(lvals)) = raise Fail "n"
            | tr (D(lvals)) = raise Fail "d"
              (* should re-think here... *)
            | tr (LList(e)) = LList(e)
            | tr (Tree(e)) = Tree(e)
            | tr (Pred(id, e)) = Pred(id, e)
            | tr (Let(e1, e2, e3)) = Let(e1, e2, e3)
      in  tr e
      end
  and opt_l l =
      let fun cast (Lval(lval)) = lval
            | cast _ = raise Fail "type bug\n"
          fun shift (lval) = Lval(lval)
          fun g (Var(id)) = shift (Var(id))
            | g (Sel(Upd(lval, e1, e2), e3))=
              let val (e1', e3') = (opt_e e1, opt_e e3)
              in  if e1' = e3'
                  then opt_e e2
                  else shift (Sel(lval, e3))
              end
            | g (Sel(Sharp(Void), e)) = shift (Sel(Sharp(Void), e))
            | g (Sel(lval, e)) =
	      let val lval' = cast(opt_l lval)
		  val e' = opt_e e
	      in  if lval<>lval' orelse e<>e'
	          then opt_l (Sel(lval', e'))
	          else shift (Sel(lval, e))
	      end
(*            | g (Sel(lval, e)) = shift (Sel(cast(opt_l lval), e))*)
            | g (Upd(lval, e1, e2)) = shift (Upd(lval, e1, e2))
            | g (Sharp(t)) = shift (Sharp(t))
            | g _ = raise Fail "these cases should not exist\n"
      in  g l
      end

      (*----------------------------- the 2-nd pass ------------------------------*)
  fun opt2_e e =
      let fun tr (Expvoid) = Expvoid
            | tr (IntNum(i)) = IntNum(i)
            | tr (True) = True
            | tr (False) = False
            | tr (Null) = Null
            | tr (BinopExp(e1, Band, e2)) =
              let fun toList (BinopExp(e1, Band, e2)) = (toList e1) @ (toList e2)
                    | toList y = [y]
                       fun fromList [] = raise Fail "don't apply to empty list\n"
                         | fromList [x] = x
                         | fromList (x::xs) = BinopExp(x, Band, fromList xs)
                       val new_e = toList (BinopExp(e1, Band, e2))
                       fun exists l e = List.exists (fn x => (x=e)) l
                       fun reduce(dst, []) = dst
                         | reduce(dst, [x]) = x::dst
                         | reduce(dst, x::xs) = if (exists xs x) then reduce(dst, xs) else reduce(x::dst, xs)
                   in  fromList(rev(reduce([], new_e)))
                   end
            | tr (BinopExp(e1, b, e2)) = BinopExp(e1, b, e2)
            | tr (Not(e)) = Not(e)
            | tr (Lval(lval)) = Lval(lval)
            | tr (Imply(e1, e2)) = Imply(opt2_e e1, opt2_e e2)
            | tr (Forall(tid, ty, e1)) = Forall(tid, ty, opt2_e e1)
            | tr (Exists(tid, ty, e1)) = Exists(tid, ty, opt2_e e1)
            | tr (Prev(lval)) = raise Fail "not implemented yet...prev"
            | tr (Pi(lvalss)) = raise Fail "pi"
            | tr (N(lvals)) = raise Fail "n"
            | tr (D(lvals)) = raise Fail "d"
            (* should re-think here... *)
            | tr (LList(lval)) = LList(lval)
            | tr (Tree(lval)) = Tree(lval)
            | tr (Pred(id, e)) = Pred(id, e)
            | tr (Let(e1, e2, e3)) = Let(e1, e2, e3)
      in  tr e
      end

  fun first vc =
      let val n_vc = ref vc
          fun loop () =
              let val res = (*if ((!n)=1) then*) opt_e (!n_vc) (*else opt2_e (!n_vc)*)
              in  if res = (!n_vc)
                  then res
                  else (n_vc:=res; loop())
              end
      in  loop()
      end

  fun second vc =
      let val n_vc = ref vc
          fun loop () =
              let val res = (*if ((!n)=1) then*) opt2_e (!n_vc) (*else opt2_e (!n_vc)*)
              in  if res = (!n_vc)
                  then res
                  else (n_vc:=res; loop())
              end
      in  loop()
      end

  fun topOpt vc =
      let val opt_vc = first vc
      in  if (!opt2)
          then second opt_vc
          else opt_vc
      end

  fun pp_ty ty =
      case ty
       of Int => "Int"
        | Bool => "Bool"
        | Void => "Void"
        | Struct s => "struct_"^s
        | Pointer ty => String.concat ["star_", pp_ty ty]
        | Array (i, ty) => String.concat ["array", Int.toString i, pp_ty ty]

  val emptyset = S.empty

  fun collecVar_exp e =
      let fun pp(Expvoid) = emptyset
            | pp(IntNum(i)) = emptyset
            | pp(True) = emptyset
            | pp(False) = emptyset
            | pp(Null) = emptyset
            | pp(Lval(lval)) = collecVar_lval lval
            | pp(BinopExp(e1, b, e2)) = S.union(collecVar_exp e1 ,collecVar_exp e2)
            | pp(Not(exp)) = collecVar_exp exp
    	    | pp(Forall(id, mytype, exp)) =
    	      let val tmp = collecVar_exp exp
    	      in  if S.member(tmp, id)
    	          then S.delete(tmp, id)
    	          else tmp
    	      end
    	    | pp(Exists(id,mytype,exp)) =
    	      let val tmp = collecVar_exp exp
    	      in  if S.member(tmp, id)
    	          then S.delete(tmp, id)
    	          else tmp
    	      end
            | pp(Imply(e1, e2)) = S.union(collecVar_exp e1,collecVar_exp e2)
            | pp (LList(exp)) = collecVar_exp exp
            | pp (Tree(exp)) = collecVar_exp exp
            | pp (Pred(id, exp)) = collecVar_exp exp
            | pp (Let(e1, e2, e3)) = S.union(S.union(collecVar_exp e1,collecVar_exp e2), collecVar_exp e3)
            | pp(_) = (raise Fail ("not implemented\n"); emptyset)
      in  pp e
      end
  and collecVar_lval lval =
      case lval
       of Var id => S.add (emptyset, id)
        | Ptr (lval1, lval2) => S.union(collecVar_lval lval1 ,collecVar_lval lval2)
        | Sharp ty => S.add(emptyset, String.concat ["ty_", pp_ty ty])
        | Inarray (lval, exp) => raise Fail "in array\n"
        | Instruct (lval, id) => (print "Coqize.56: in struct\n"; emptyset)
        | Instruct2 (lval, id1, id2) => (print "Coqize.57: in struct\n"; emptyset)
        | Upd (lval1, e1, e2) => S.union(collecVar_lval lval1,S.union(collecVar_exp e1,collecVar_exp e2))
        | Sel (lval1, e) => S.union(collecVar_lval lval1, collecVar_exp e)

  fun pp_b(Plus) = "+"
    | pp_b(Minus) = "-"
    | pp_b(Times) = "*"
    | pp_b(Divide) = "/"
    | pp_b(Modus) = raise Fail ("not implemented\n")
    | pp_b(Band) = "/\\"
    | pp_b(Bor) = "\\/"
    | pp_b(Equ) = "="
    | pp_b(NEqu) = "<>"
    | pp_b(GT) = ">"
    | pp_b(GE) = ">="
    | pp_b(LT) = "<"
    | pp_b(LE) = "<="

  fun pp_exp e =
      let fun pp(Expvoid) = "expvoid" (*raise Fail (s^"expvoid\n")*)
            | pp(IntNum(i)) = (Int.toString i)
            | pp(True) = "True"
            | pp(False) = "False"
            | pp(Null) = "0"
            | pp(Lval(lval)) = ""^(pp_lval lval)^""  (* maybe a bug in some cases... -Baojian*)
            | pp(BinopExp(e1, b, e2)) = "("^(pp_exp e1)^")"^(pp_b b)^"("^(pp_exp e2)^")"
            | pp(Not(e)) = "~("^(pp_exp e)^")"
            | pp(Imply(e1, e2)) = "("^(pp_exp e1)^(") -> (")^(pp_exp e2)^")"
            | pp(Forall(id, ty, e)) = "forall "^id^" : Z, "^(pp_exp e)
            | pp(Exists(id, ty, e)) = "exists "^id^" : Z. "^(pp_exp e)
            | pp (LList(exp)) = "list("^(pp_exp exp)^")"
            | pp (Tree(exp)) = "tree("^(pp_exp exp)^")"
            | pp (Pred(id, exp)) = id^"("^(pp_exp exp)^")"
            | pp (Let(e1, e2, e3)) = "let "^(pp_exp e1)^" = "^(pp_exp e2)^" in "^(pp_exp e3)^" end"
            | pp(_) = raise Fail ("not implemented\n")
      in  pp e
      end
  and pp_lval lval =
      case lval
       of Var id => id
        | Upd (lval, e1, e2) => ("upd(")^(pp_lval lval)^(", ")^(pp_exp e1)^(", ")^(pp_exp e2)^(")")
        | Sel (lval, e) => "sel("^(pp_lval lval)^", "^(pp_exp e)^")"
        | Sharp (ty) => "ty_"^(pp_ty ty)
        | Ptr (lval1, lval2) => "ptr("^(pp_lval lval1)^", "^(pp_lval lval2)^")"
        | Inarray (lval, exp) => (raise Fail "in array\n")
        | Instruct (lval, id) => (print "Coqize.104: in struct\n"; "")
        | Instruct2 (lval, id1, id2) => String.concat [pp_lval lval, "(->", id1, ")", id2]

  fun var_out set =
    let val var_list = S.listItems set
        fun out([]) =""
          | out(x::xs) = x^" "^out(xs)
    in out var_list
    end

  fun V_out vc =
    let val s=var_out(collecVar_exp vc)
    in if(s="") then ""
       else ("forall "^s^": Z, ")
    end

  fun one (name, vc) = ("Lemma "^(Id.toString name)^"_vc"^": ")^V_out(vc)^(pp_exp vc)^".\n\n\n"

  fun ppTop (strVcList, i) =
      let val strStr = List.map one strVcList
          val vcstri = (Coqlib.libs())^(String.concat strStr)
          fun get() = File.nameToString (!ErrorMsg.file)
          val outfile = File.creat (String.concat [get (), Int.toString i, ".v"])
      in  File.write (outfile, vcstri)
      end
  (*
  fun forall_one vc =
      let val id_list = S.listItems (collecVar_exp vc)*)
           (* the type is not correct, do we really need a precise one? *)
          (*fun add [] dst = dst
            | add (x::xs) dst = add xs (Vc.Forall(x, Vc.Void, dst))
      in  add id_list vc
      end
  fun forallize [] = []
    | forallize ((name, vc)::xs) = (name, forall_one vc)::(forallize xs)*)
end
